Parametric Sort #111

Shoooooon · 2024-02-22T01:16:57Z

Partial support for ArraysEX theory added
JSON output for parametric sorts defined:
- Sorts are identifiers or objects of the form { "sortKind": (identifier), "sortParams": [sort...] }
- e.g., Int, [Bitvec, 32], { "sortKind": Array, "sortParams": [Int, Int]}
- Nonterminals are handled/printed as sorts as well, so I opted to avoid changing the representation of unparametrized identifiers.

…rminals being treated as sorts. Added array integration test.

kjcjohnson · 2024-02-23T01:36:33Z

I am, in general, fine with this PR - looks good to me.

I do want to be a bit pedantic about naming on the JSON format changes.

sortKind and sortParams should just be kind and params. We're already inside of a sort object, so it's redundant to have sort in the name! In most places it's used, it will be as a parameter called sort: or returnSort: or similar.
Why kind? The SMT-LIB docs seem to mostly call it the "sort symbol", and we use "name" and "id" in other similar places. It's fine if you have a justification, but just want to be intentional about it. It will be difficult to change in the future :)

Shoooooon · 2024-02-23T01:55:27Z

I agree about changing sortKind and sortParams to kind and params.
I tried to stay away from "name" and "id" because the kind is not unique to a given sort (e.g., one might have (Set Int) and (Set Bool), in which case name and id are a little misleading). The phrase "symbol" misses the point that the kind defines the overarching type of the object.

kjcjohnson and others added 3 commits February 20, 2024 19:48

Support the Array sort (but no functions yet)

963c56a

Updated JSON output format for parametric sorts.

486a126

Changed JSON parametric sort format to eliminate conflicts with nonte…

a7d6999

…rminals being treated as sorts. Added array integration test.

Changed sortKind and sortParam to kind and param.

a828b3e

kjcjohnson merged commit 884868e into SemGuS-git:main Feb 23, 2024
7 checks passed

Provide feedback